TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict Trs: { lineMult(n, nil(), l2) -> nil() , lineMult(n, ::(x, xs), nil()) -> ::(*(x, n), lineMult(n, xs, nil())) , lineMult(n, ::(x, xs), ::(y, ys)) -> ::(+(*(x, n), y), lineMult(n, xs, ys)) , *(0(), y) -> 0() , *(s(x), y) -> +(y, *(x, y)) , +(0(), y) -> y , +(s(x), y) -> s(+(x, y)) , computeLine(nil(), m, acc) -> acc , computeLine(::(x, xs), nil(), acc) -> nil() , computeLine(::(x, xs), ::(l, ls), acc) -> computeLine(xs, ls, lineMult(x, l, acc)) , matrixMult(nil(), m2) -> nil() , matrixMult(::(l, ls), m2) -> ::(computeLine(l, m2, nil()), matrixMult(ls, m2)) } Obligation: runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 300.0 seconds. Arrrr..